\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).\+
\\[0ex]Trans($T$;$a$,$b$.$R$($a$,$b$))
\\[0ex]$\Rightarrow$ \{$\forall$$a$, $b$, $c$:$T$. strict\_part($x$,$y$.$R$($x$,$y$);$a$;$b$) $\Rightarrow$ $R$($b$,$c$) $\Rightarrow$ strict\_part($x$,$y$.$R$($x$,$y$);$a$;$c$)\}
\-
\end{tabbing}